$\forall$$T$:Type, $L$:$T$ List, $i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$.
\\[0ex]$\exists$$L_{2}$:$T$ List, $f_{1}$:($\mathbb{N}$$_{\mbox{\scriptsize $<$1}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$), $f_{2}$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{2}$$\parallel$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$).
\\[0ex]interleaving\_occurence($T$;[$L$[$i$]];$L_{2}$;$L$;$f_{1}$;$f_{2}$) \& $f_{1}$(0) $=$ $i$ $\in$ $\mathbb{Z}$